Widening gas #1442

Red-Panda64 · 2024-05-03T10:39:20Z

Description

This PR adds widening gas to the td3 solver. Widening gas permits an unknown to grow N times and still be combined with the regular join. Only once the unknown runs out of gas, the widening operator is used. Widening gas can be applied to regular unknowns and leaf unknowns.
Additionally, this PR extracts the side_widen strategies out of the main solve routine and wraps them in an interface.

Config Options

The gas budget for regular unknowns is controlled via solvers.td3.widen_gas, whereas leaves are controlled via solvers.td3.side_widen_gas. Both config options are 0 by default, effectively disabling the feature.
When widening points are configured to be reset with the solvers.td3.remove-wpoint option, this too resets that wpoints gas.

New side_widen Interface and Gas for Leaves

Widening gas co-exists with the other side-widening strategies.
Side widen strategies are meant to determine, when a leaf becomes a widening point. After a leaf has been selected as widening point, future updates to its value are applied with the widen operator. The widening gas can again be used to postpone this:
After a leaf has been marked as widening point, its gas counter is decreased for every increase to its value. Once it hits 0, widening is applied.

There is one exception, namely the side_widen strategy sides-local. It does not mark widening points, instead widening only if the incoming side-effect is larger than a previous side-effect that came from the same unknown. This has been adapted to work with widening gas like so: every time that the sides-local strategy would widen, the gas is decremented.

Functions of the new interface:

module type WPointSelect =
    sig
      type data

      (** Create data required by this widening point selection strategy.
          The parameters are not necessarily used by all strategies. 
      *)
      val create_data: (S.v -> bool) -> (S.v -> S.v -> unit) -> data
      (** Notifies this strategy that a side-effect has occured.
          This allows the strategy to adapt its internal data structure.
      *)
      val notify_side: data -> S.v option -> S.v -> unit
      (** Whether the destabilization of the side-effected var should record the destabilization
          of called variables and start variables. This information should be passed to [should_mark_wpoint].
      *)
      val record_destabilized_vs: bool
      (** This strategy can decide to prevent widening.
          Note that, if this strategy does not veto, this does not mean that widening
          will necessarily be performed. Nor does a call to this function imply that
          the value of the leaf has grown.
      *)
      val veto_widen: data -> unit HM.t -> VS.t -> S.v option -> S.v -> bool
      (** The value of the leaf has grown. Should it be marked a widening point?
          Even if this function is called, leaf y might already be a widening point
          from an earlier side-effect.
      *)
      val should_mark_wpoint: data -> unit HM.t -> VS.t -> S.v option -> S.v -> bool option -> bool
    end

Note that notify_side is needed for unstable-self, which records side-effects in the infl set. veto_widen is necessary to implement the above behavior for sides-local. record_destabilized_vs is currently only used by the cycle strategy. It indicates, whether the more expensive version of destabilize needs to be called, which also records whether a called or start variable was destabilized.

sim642 · 2024-05-03T10:51:45Z

Why does this need to be inside the solver? This sounds like widening delay, which can be completely solver-independent and can be implemented simply as a lifting of a domain (overriding its widen).

michael-schwarz · 2024-05-03T11:06:11Z

@sim642 One could implement a similar feature as a domain lifter, yes. However, the effect would be subtly different: Here the delay (gas) is applied per unknown, whereas tracking it in the domain would mean that the gas value is propagated, e.g., between different loops, or that a complicated mechanism tracking not just one gas value but several inside a map would be required.
In the scope of this thesis, we investigate ideas for integrating a widening gas into the solver as a generalization of its automatic widening point detection which aims to be completely transparent to the writer of the analyses.
We are particularly interested in the values at globals here (but include it for locals for the sake of completeness). @Red-Panda64 will later on also implement a narrowing on globals in order to compare both approaches to having more precise globals.
The strategy of having delays tracked inside the domain is also interesting, and it may be worth comparing the impacts of both some time after the thesis is finished.

sim642 · 2024-05-03T13:15:09Z

@sim642 One could implement a similar feature as a domain lifter, yes. However, the effect would be subtly different: Here the delay (gas) is applied per unknown, whereas tracking it in the domain would mean that the gas value is propagated, e.g., between different loops, or that a complicated mechanism tracking not just one gas value but several inside a map would be required.

I think the standard implementation is just domain lifting where transfer functions set the counter to 0, so none of such propagation occurs.

I'm again worried about the monolithic growth of the TD3 solver. For a long time we've wanted to undo that monolithic structure into a more modular one. While nobody has worked on decomposing the existing solver, at some point we decided to not worsen the problem and implement new things modularly. For example, DepVals is just a lifter for the solver and this could easily be as well.

Red-Panda64 · 2024-05-06T09:18:10Z

This seems like a policy discussion, so I cannot really say much.
However, as @michael-schwarz said, the widening gas will probably mainly be meaningful for globals, so it's good to control the gas of globals and locals independently. This would be difficult to do when baking it not the domain, right?

sim642 · 2024-05-06T09:58:06Z

However, as @michael-schwarz said, the widening gas will probably mainly be meaningful for globals, so it's good to control the gas of globals and locals independently. This would be difficult to do when baking it not the domain, right?

I think it would even be easier: one can choose whether to wrap an analysis's module D or/and module G with such a lifter. Either at a global level or even on a per-analysis level.

sim642 · 2024-05-14T11:59:18Z

We discussed this during GobCon and here's the summary.

Currently, module type WPointSelect and all of its various implementations are somewhat deep in the Td3.Base module itself, but the logic that they implement is rather independent of the solver as a whole. They seem to be more-or-less functions on constraint system unknowns (S.v).
It would be good if they could be hoisted up (e.g. line 42 of td3.ml). It was pointed out that they still depend on S.v type and S.Var module for some operations, so they might need to be turned into functors with S.Var as the argument to make such hoisting possible. Hopefully this is then possible.

The change from wpoint: unit HM.t to wpoint_gas: int HM.t isn't much of a concern. Especially because unit HM.t stores unit values (basically ints 0) for values already, so this generalizes the data structure for all of the widenings but shouldn't incur any overhead to the cases when no gas is used.

Some small style improvements should also be done to make this merge-ready. It was mentioned that there are some parentheses which are unneeded (e.g. around if .. then conditions).

Red-Panda64 · 2024-05-21T10:12:20Z

I have extracted the modules out of td3.Base. For now, I have placed them in their own module in src/solver. Since this directory so far only contains solver implementations, I am not sure if it is a good place for them. However, I cannot really see any other place they would belong, because they exclusively affect the solving algorithm. Any opinions on this?

but the logic that they implement is rather independent of the solver as a whole.

So far, no other solver implements these strategies, so I have left the selection of the concrete implementation in td3. In their current form, I would not say that the strategies are really independent from td3. Some of the functions/strategies need td3-specific details, like an add_infl function, or data structures like the stable and called sets. I think it would be preferable to have them out of the td3.Base module but inside td3.

src/solver/td3.ml

sim642 · 2024-05-22T07:21:26Z

src/solver/td3.ml

+            (* is there a reason for the redundant widen check? *)
+            if tracing && not (S.Dom.is_bot old) && should_widen x then trace "solchange" "%a (wpx: %b): %a" S.Var.pretty_trace x (should_widen x) S.Dom.pretty_diff (wpd, old);


What is this comment about?

My comment is strangely worded, but I think it is odd that should_widen or previously HM.mem wpoint x is re-evaluated here.
Specifically, let wp = should_widen x before evaluating eq is used to determine, whether widening should be applied. The result of should_widen may have changed through eq, yet I would assume the value that is logged should reflect the value that is used for the actual widening decision.

But if using the updated value, I should be logging with format_wpoint, which will not only show whether x is a wpoint, but also how much gas it has.

Reusing wp seems sensible here indeed.

src/solver/td3.ml

src/solver/sideWPointSelect.ml

src/solver/td3.ml

sim642 · 2024-05-22T07:54:08Z

I have extracted the modules out of td3.Base. For now, I have placed them in their own module in src/solver. Since this directory so far only contains solver implementations, I am not sure if it is a good place for them. However, I cannot really see any other place they would belong, because they exclusively affect the solving algorithm. Any opinions on this?

It would've been fine to leave them in td3.ml, but a separate file might even be better. That directory already has other solver-specific helper modules anyway (e.g. SolverBox).

for globals unknowns: * can be used together with other widening strategies * reduce gas whenever global grows * widen only if marked as widening point by side_widen and gas is 0

sim642 · 2025-01-17T13:19:28Z

src/solver/td3.ml

@@ -275,6 +281,21 @@ module Base =
      let destabilize_ref: (S.v -> unit) ref = ref (fun _ -> failwith "no destabilize yet") in
      let destabilize x = !destabilize_ref x in (* must be eta-expanded to use changed destabilize_ref *)

+      let format_wpoint x = Option.map_default (fun x -> Printf.sprintf "true (gas: %d)" x) "false" (HM.find_option wpoint_gas x) in


If this is just used for tracing, then something like the following would be nicer:

Suggested change

let format_wpoint x = Option.map_default (fun x -> Printf.sprintf "true (gas: %d)" x) "false" (HM.find_option wpoint_gas x) in

let pretty_wpoint () x =

match HM.find_option wpoint_gas x with

| None -> Pretty.text "false"

| Some x -> Pretty.dprintf "true (gas: %d)" x

in

(Don't commit this directly, I have not typechecked this.)

That can be used in tracing with %a. It avoids the lookup and string construction if tracing is enabled but something other is being traced. Otherwise unnecessary garbage is created.

sim642 · 2025-01-17T13:20:55Z

src/solver/td3.ml

-            else if term then
-              match phase with
-              | Widen -> S.Dom.widen old (S.Dom.join old eqd)
-              | Narrow when GobConfig.get_bool "exp.no-narrow" -> old (* no narrow *)
-              | Narrow ->
-                (* assert S.Dom.(leq eqd old || not (leq old eqd)); (* https://github.com/goblint/analyzer/pull/490#discussion_r875554284 *) *)
-                S.Dom.narrow old eqd
-            else
-              box old eqd
+            else (
+              if term then
+                match phase with
+                | Widen -> S.Dom.widen old (S.Dom.join old eqd)
+                | Narrow when GobConfig.get_bool "exp.no-narrow" -> old (* no narrow *)
+                | Narrow ->
+                  (* assert S.Dom.(leq eqd old || not (leq old eqd)); (* https://github.com/goblint/analyzer/pull/490#discussion_r875554284 *) *)
+                  S.Dom.narrow old eqd
+              else (
+                box old eqd
+              )
+            )


This seems to be just changing the formatting which would be nice to not change unnecessarily.

michael-schwarz requested a review from stilscher May 3, 2024 10:45

michael-schwarz added precision feature student-job labels May 3, 2024

michael-schwarz linked an issue May 8, 2024 that may be closed by this pull request

Solver TD3-💨 with Side-Effect Gas #1358

Open

sim642 reviewed May 22, 2024

View reviewed changes

sim642 mentioned this pull request May 29, 2024

Implement delayed widening #1483

Open

2 tasks

Red-Panda64 added 2 commits December 3, 2024 14:15

implement solver-based widening delay for td3

2177e0a

for globals unknowns: * can be used together with other widening strategies * reduce gas whenever global grows * widen only if marked as widening point by side_widen and gas is 0

fix whitespace errors

493732e

Red-Panda64 force-pushed the widening-gas branch from b65cdc3 to 493732e Compare December 3, 2024 13:19

Red-Panda64 mentioned this pull request Dec 3, 2024

Narrowing of globals in TD #1636

Open

sim642 self-requested a review January 3, 2025 08:57

sim642 reviewed Jan 17, 2025

View reviewed changes

sim642 added this to the v2.6.0 milestone Jan 17, 2025

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Widening gas #1442

Widening gas #1442

Red-Panda64 commented May 3, 2024

sim642 commented May 3, 2024

michael-schwarz commented May 3, 2024

sim642 commented May 3, 2024

Red-Panda64 commented May 6, 2024

sim642 commented May 6, 2024

sim642 commented May 14, 2024

Red-Panda64 commented May 21, 2024

sim642 May 22, 2024

Red-Panda64 May 22, 2024 •

edited

Loading

sim642 Jan 17, 2025

sim642 commented May 22, 2024

sim642 Jan 17, 2025

sim642 Jan 17, 2025

		(* is there a reason for the redundant widen check? *)
		if tracing && not (S.Dom.is_bot old) && should_widen x then trace "solchange" "%a (wpx: %b): %a" S.Var.pretty_trace x (should_widen x) S.Dom.pretty_diff (wpd, old);

-      let format_wpoint x = Option.map_default (fun x -> Printf.sprintf "true (gas: %d)" x) "false" (HM.find_option wpoint_gas x) in
+      let pretty_wpoint () x =
+        match HM.find_option wpoint_gas x with
+        | None -> Pretty.text "false"
+        | Some x -> Pretty.dprintf "true (gas: %d)" x
+      in

Widening gas #1442

Are you sure you want to change the base?

Widening gas #1442

Conversation

Red-Panda64 commented May 3, 2024

Description

Config Options

New side_widen Interface and Gas for Leaves

sim642 commented May 3, 2024

michael-schwarz commented May 3, 2024

sim642 commented May 3, 2024

Red-Panda64 commented May 6, 2024

sim642 commented May 6, 2024

sim642 commented May 14, 2024

Red-Panda64 commented May 21, 2024

sim642 May 22, 2024

Choose a reason for hiding this comment

Red-Panda64 May 22, 2024 • edited Loading

Choose a reason for hiding this comment

sim642 Jan 17, 2025

Choose a reason for hiding this comment

sim642 commented May 22, 2024

sim642 Jan 17, 2025

Choose a reason for hiding this comment

sim642 Jan 17, 2025

Choose a reason for hiding this comment

Red-Panda64 May 22, 2024 •

edited

Loading